*****∀E walk home,desk,car,I,S0;

1 (walkable(home)∧((att(desk,home)∨holds(at(desk,home),S0))∧((att(car,home)∨holds(at(car,home),S0))∧holds(at(I,d%
esk),S0))))⊃(holds(at(I,car),result(I,walk(car),S0))∧∀x y.(¬(x=I)⊃(holds(at(x,y),result(I,walk(car),S0))≡holds(a%
t(x,y),S0))))  

*****∀E drive county,home,airport,I,result(I,walk(car),S0);

2 (drivable(county)∧(att(home,county)∧(att(airport,county)∧(holds(at(car,home),result(I,walk(car),S0))∧holds(at(%
I,car),result(I,walk(car),S0))))))⊃(holds(at(car,airport),result(I,drive(airport),result(I,walk(car),S0)))∧∀x y.%
((¬(x=car∨holds(at(x,car),result(I,walk(car),S0)))∨y=car)⊃(holds(at(x,y),result(I,drive(airport),result(I,walk(c%
ar),S0)))≡holds(at(x,y),result(I,walk(car),S0)))))  

*****∀E attrans1 I,car,airport,result(I,drive(airport),result(I,walk(car),S0));

3 (holds(at(I,car),result(I,drive(airport),result(I,walk(car),S0)))∧holds(at(car,airport),result(I,drive(airport%
),result(I,walk(car),S0))))⊃holds(at(I,airport),result(I,drive(airport),result(I,walk(car),S0)))  

*****TAUTEQ ∀x y.(¬(x=I)⊃(holds(at(x,y),result(I,walk(car),S0))≡holds(at(x,y),S0))) walkable,at1,at2,at3,1;

4 ∀x y.(¬(x=I)⊃(holds(at(x,y),result(I,walk(car),S0))≡holds(at(x,y),S0)))  

*****∀E ↑ car,home;

5 ¬(car=I)⊃(holds(at(car,home),result(I,walk(car),S0))≡holds(at(car,home),S0))  

*****TAUTEQ ∀x y.((¬(x=car∨holds(at(x,car),result(I,walk(car),S0)))∨y=car)⊃(holds(at(x,y),result(I,drive(airport%
),result(I,walk(car),S0)))≡holds(at(x,y),result(I,walk(car),S0)))) walkable,drivable,at1,at2,at3,at4,at5,notI,1:%
5;

6 ∀x y.((¬(x=car∨holds(at(x,car),result(I,walk(car),S0)))∨y=car)⊃(holds(at(x,y),result(I,drive(airport),result(I%
,walk(car),S0)))≡holds(at(x,y),result(I,walk(car),S0))))  

*****∀E ↑ I,car;

7 (¬(I=car∨holds(at(I,car),result(I,walk(car),S0)))∨car=car)⊃(holds(at(I,car),result(I,drive(airport),result(I,w%
alk(car),S0)))≡holds(at(I,car),result(I,walk(car),S0)))  

*****TAUTEQ holds(at(I,airport),result(I,drive(airport),result(I,walk(car),S0))) notI,walkable,drivable,at1,at2,%
at3,at4,at5,1:7;

8 holds(at(I,airport),result(I,drive(airport),result(I,walk(car),S0)))  

*****∀E prog walk(car),drive(airport),I,S0;

9 result(I,prog(walk(car),drive(airport)),S0)=result(I,drive(airport),result(I,walk(car),S0))  

*****SUBSTR ↑ IN ↑↑;

10 holds(at(I,airport),result(I,prog(walk(car),drive(airport)),S0))  

*****∀E should I,at(I,airport),prog(walk(car),drive(airport)),S0;

11 (wants(I,at(I,airport),S0)∧holds(at(I,airport),result(I,prog(walk(car),drive(airport)),S0)))⊃should(I,prog(wa%
lk(car),drive(airport)),S0)  

*****TAUT should(I,prog(walk(car),drive(airport)),S0) want,10:11;

12 should(I,prog(walk(car),drive(airport)),S0)